(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
0(0(1(x1))) → 0(0(2(1(x1))))
0(1(3(x1))) → 0(3(4(1(x1))))
3(1(1(x1))) → 3(1(4(1(x1))))
3(1(1(x1))) → 3(4(1(4(4(1(x1))))))
3(1(1(x1))) → 3(4(4(1(2(4(1(x1)))))))
3(3(1(x1))) → 3(2(1(3(x1))))
5(0(4(x1))) → 4(0(5(4(x1))))
0(0(0(1(x1)))) → 0(0(0(2(1(x1)))))
0(0(1(5(x1)))) → 0(0(5(1(2(4(x1))))))
0(0(5(3(x1)))) → 0(0(5(4(3(x1)))))
0(4(1(1(x1)))) → 0(5(4(1(2(1(x1))))))
0(4(3(1(x1)))) → 0(3(5(4(1(x1)))))
0(4(3(4(x1)))) → 0(3(2(4(4(x1)))))
3(0(1(1(x1)))) → 0(2(1(3(1(x1)))))
3(1(1(5(x1)))) → 3(1(2(1(5(x1)))))
5(0(1(5(x1)))) → 0(5(4(1(5(x1)))))
5(2(3(1(x1)))) → 4(5(2(1(3(x1)))))
5(2(3(5(x1)))) → 2(4(5(3(5(x1)))))
5(2(5(4(x1)))) → 2(4(5(4(5(x1)))))
0(1(2(2(1(x1))))) → 2(4(0(1(2(1(x1))))))
0(1(5(0(4(x1))))) → 0(2(1(5(4(0(x1))))))
0(1(5(5(3(x1))))) → 0(5(4(5(1(3(x1))))))
0(2(2(1(5(x1))))) → 0(2(1(5(4(2(4(4(2(x1)))))))))
0(2(2(3(4(x1))))) → 0(3(4(4(2(4(4(2(x1))))))))
0(2(5(1(1(x1))))) → 5(0(1(2(4(1(x1))))))
0(3(3(2(3(x1))))) → 0(3(3(2(4(3(x1))))))
0(4(4(3(4(x1))))) → 4(4(4(4(0(3(x1))))))
3(0(1(4(3(x1))))) → 3(2(0(3(4(1(x1))))))
3(0(4(5(1(x1))))) → 3(5(4(4(1(0(x1))))))
3(1(1(1(2(x1))))) → 3(2(1(4(1(2(1(2(x1))))))))
5(2(3(1(4(x1))))) → 5(2(1(2(1(3(4(x1)))))))
5(3(0(0(4(x1))))) → 0(0(3(5(4(4(x1))))))
0(1(3(4(3(4(x1)))))) → 0(3(4(3(4(1(2(x1)))))))
0(1(5(0(4(2(x1)))))) → 0(5(2(4(1(0(2(x1)))))))
0(2(2(2(3(1(x1)))))) → 0(2(2(4(2(3(1(x1)))))))
0(4(1(1(0(4(x1)))))) → 0(4(4(1(4(1(0(x1)))))))
0(4(3(2(2(3(x1)))))) → 0(2(3(2(4(2(3(x1)))))))
3(0(4(1(2(2(x1)))))) → 3(2(1(0(4(4(2(x1)))))))
3(1(0(3(5(4(x1)))))) → 3(0(3(2(1(5(4(x1)))))))
3(2(2(1(1(3(x1)))))) → 1(2(1(3(2(4(3(x1)))))))
3(3(3(1(3(5(x1)))))) → 3(2(1(3(3(3(5(x1)))))))
3(4(3(0(4(5(x1)))))) → 3(5(0(3(4(4(4(x1)))))))
3(4(3(1(4(2(x1)))))) → 3(4(2(1(3(2(2(4(2(4(x1))))))))))
3(5(0(2(1(4(x1)))))) → 3(2(4(0(5(1(2(x1)))))))
3(5(5(2(3(1(x1)))))) → 5(5(4(3(3(2(1(x1)))))))
5(0(1(2(3(1(x1)))))) → 2(1(0(3(4(5(4(4(4(1(x1))))))))))
5(0(4(3(3(1(x1)))))) → 0(3(5(1(5(4(4(3(x1))))))))
0(0(1(1(3(3(3(x1))))))) → 0(3(0(1(3(3(4(1(x1))))))))
0(0(2(5(1(4(2(x1))))))) → 0(2(1(0(5(4(2(2(x1))))))))
0(2(5(4(4(1(5(x1))))))) → 1(2(4(5(0(5(4(4(x1))))))))
0(4(2(3(4(5(4(x1))))))) → 3(0(5(4(4(2(4(0(x1))))))))
0(5(2(1(2(1(4(x1))))))) → 2(1(2(1(0(5(2(4(x1))))))))
3(2(5(0(4(0(1(x1))))))) → 0(0(5(4(2(2(4(4(1(3(x1))))))))))
3(4(3(4(0(1(4(x1))))))) → 3(4(2(4(4(4(0(5(1(2(3(x1)))))))))))
3(5(2(1(0(2(2(x1))))))) → 2(1(3(0(5(2(2(4(x1))))))))
3(5(2(2(0(1(1(x1))))))) → 3(2(4(5(0(2(1(2(1(x1)))))))))
3(5(3(4(0(1(4(x1))))))) → 2(1(5(4(3(4(0(3(x1))))))))
5(1(5(3(1(1(3(x1))))))) → 2(1(5(1(5(1(3(3(x1))))))))
5(2(0(0(1(0(3(x1))))))) → 0(5(3(4(2(1(0(0(x1))))))))
5(2(0(4(0(4(3(x1))))))) → 2(0(5(1(0(4(4(3(x1))))))))
5(2(3(0(0(4(3(x1))))))) → 0(5(4(2(4(3(0(3(3(x1)))))))))
5(2(3(3(2(0(5(x1))))))) → 2(0(3(3(5(2(4(5(x1))))))))
5(5(5(0(1(4(3(x1))))))) → 0(5(4(4(3(4(5(5(1(x1)))))))))
0(2(0(5(5(2(2(3(x1)))))))) → 5(2(2(4(5(3(2(0(0(x1)))))))))
0(2(5(2(4(0(1(4(x1)))))))) → 0(3(0(5(2(1(2(2(4(4(x1))))))))))
0(4(1(5(3(2(3(3(x1)))))))) → 0(5(4(1(2(3(3(4(3(x1)))))))))
0(4(5(0(1(5(2(3(x1)))))))) → 2(1(2(4(2(5(3(0(5(0(x1))))))))))
0(5(5(1(4(2(0(3(x1)))))))) → 0(3(5(1(2(0(5(1(2(4(x1))))))))))
3(0(1(3(2(0(4(2(x1)))))))) → 0(4(2(2(2(4(1(0(3(3(4(x1)))))))))))
3(3(1(1(2(5(5(2(x1)))))))) → 3(2(1(5(1(2(5(3(1(x1)))))))))
3(5(4(2(5(1(0(4(x1)))))))) → 4(2(4(2(1(3(5(0(5(4(x1))))))))))
5(0(4(3(0(2(2(3(x1)))))))) → 0(2(4(4(0(3(2(5(3(x1)))))))))
5(2(2(0(4(0(1(4(x1)))))))) → 4(2(4(0(0(5(1(0(2(x1)))))))))
5(2(2(0(4(1(5(4(x1)))))))) → 2(5(2(4(5(0(2(1(4(x1)))))))))
5(3(2(2(1(1(0(5(x1)))))))) → 0(3(2(5(2(1(5(1(2(x1)))))))))
0(0(4(4(5(3(1(1(5(x1))))))))) → 2(1(5(4(4(4(1(0(0(3(5(x1)))))))))))
0(1(2(5(1(4(0(3(4(x1))))))))) → 0(2(4(0(3(1(2(1(2(4(5(x1)))))))))))
0(1(3(1(2(0(1(1(5(x1))))))))) → 0(5(1(0(1(4(1(1(2(3(x1))))))))))
0(2(0(4(1(5(3(0(4(x1))))))))) → 4(1(0(3(5(0(0(2(2(4(x1))))))))))
0(4(3(3(4(2(5(0(5(x1))))))))) → 0(5(0(4(3(2(4(5(3(2(x1))))))))))
3(0(4(3(5(4(3(0(1(x1))))))))) → 0(3(0(3(4(3(2(4(5(1(x1))))))))))
3(1(5(3(1(1(0(3(2(x1))))))))) → 5(1(0(3(2(1(3(3(2(1(x1))))))))))
3(3(0(0(1(5(4(0(4(x1))))))))) → 1(0(2(4(4(0(3(5(0(3(x1))))))))))
5(2(0(3(1(2(5(0(4(x1))))))))) → 5(1(0(3(5(2(4(2(4(0(x1))))))))))
5(2(0(3(2(0(4(4(1(x1))))))))) → 0(5(3(0(5(2(2(4(2(4(1(x1)))))))))))
5(5(0(1(1(3(2(5(2(x1))))))))) → 3(5(1(2(2(0(5(1(5(4(x1))))))))))
5(5(3(2(1(0(1(0(4(x1))))))))) → 0(2(1(3(5(0(5(4(2(4(1(x1)))))))))))
0(1(3(1(4(2(0(4(5(2(x1)))))))))) → 4(0(1(2(4(0(2(1(5(1(3(x1)))))))))))
0(4(3(1(3(5(2(5(4(4(x1)))))))))) → 0(5(5(2(4(4(1(5(4(3(3(x1)))))))))))
3(2(0(2(0(5(2(3(4(5(x1)))))))))) → 3(5(4(4(2(0(3(2(5(2(0(x1)))))))))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(0(1(z0))) → 0(0(2(1(z0))))
0(1(3(z0))) → 0(3(4(1(z0))))
0(0(0(1(z0)))) → 0(0(0(2(1(z0)))))
0(0(1(5(z0)))) → 0(0(5(1(2(4(z0))))))
0(0(5(3(z0)))) → 0(0(5(4(3(z0)))))
0(4(1(1(z0)))) → 0(5(4(1(2(1(z0))))))
0(4(3(1(z0)))) → 0(3(5(4(1(z0)))))
0(4(3(4(z0)))) → 0(3(2(4(4(z0)))))
0(1(2(2(1(z0))))) → 2(4(0(1(2(1(z0))))))
0(1(5(0(4(z0))))) → 0(2(1(5(4(0(z0))))))
0(1(5(5(3(z0))))) → 0(5(4(5(1(3(z0))))))
0(2(2(1(5(z0))))) → 0(2(1(5(4(2(4(4(2(z0)))))))))
0(2(2(3(4(z0))))) → 0(3(4(4(2(4(4(2(z0))))))))
0(2(5(1(1(z0))))) → 5(0(1(2(4(1(z0))))))
0(3(3(2(3(z0))))) → 0(3(3(2(4(3(z0))))))
0(4(4(3(4(z0))))) → 4(4(4(4(0(3(z0))))))
0(1(3(4(3(4(z0)))))) → 0(3(4(3(4(1(2(z0)))))))
0(1(5(0(4(2(z0)))))) → 0(5(2(4(1(0(2(z0)))))))
0(2(2(2(3(1(z0)))))) → 0(2(2(4(2(3(1(z0)))))))
0(4(1(1(0(4(z0)))))) → 0(4(4(1(4(1(0(z0)))))))
0(4(3(2(2(3(z0)))))) → 0(2(3(2(4(2(3(z0)))))))
0(0(1(1(3(3(3(z0))))))) → 0(3(0(1(3(3(4(1(z0))))))))
0(0(2(5(1(4(2(z0))))))) → 0(2(1(0(5(4(2(2(z0))))))))
0(2(5(4(4(1(5(z0))))))) → 1(2(4(5(0(5(4(4(z0))))))))
0(4(2(3(4(5(4(z0))))))) → 3(0(5(4(4(2(4(0(z0))))))))
0(5(2(1(2(1(4(z0))))))) → 2(1(2(1(0(5(2(4(z0))))))))
0(2(0(5(5(2(2(3(z0)))))))) → 5(2(2(4(5(3(2(0(0(z0)))))))))
0(2(5(2(4(0(1(4(z0)))))))) → 0(3(0(5(2(1(2(2(4(4(z0))))))))))
0(4(1(5(3(2(3(3(z0)))))))) → 0(5(4(1(2(3(3(4(3(z0)))))))))
0(4(5(0(1(5(2(3(z0)))))))) → 2(1(2(4(2(5(3(0(5(0(z0))))))))))
0(5(5(1(4(2(0(3(z0)))))))) → 0(3(5(1(2(0(5(1(2(4(z0))))))))))
0(0(4(4(5(3(1(1(5(z0))))))))) → 2(1(5(4(4(4(1(0(0(3(5(z0)))))))))))
0(1(2(5(1(4(0(3(4(z0))))))))) → 0(2(4(0(3(1(2(1(2(4(5(z0)))))))))))
0(1(3(1(2(0(1(1(5(z0))))))))) → 0(5(1(0(1(4(1(1(2(3(z0))))))))))
0(2(0(4(1(5(3(0(4(z0))))))))) → 4(1(0(3(5(0(0(2(2(4(z0))))))))))
0(4(3(3(4(2(5(0(5(z0))))))))) → 0(5(0(4(3(2(4(5(3(2(z0))))))))))
0(1(3(1(4(2(0(4(5(2(z0)))))))))) → 4(0(1(2(4(0(2(1(5(1(3(z0)))))))))))
0(4(3(1(3(5(2(5(4(4(z0)))))))))) → 0(5(5(2(4(4(1(5(4(3(3(z0)))))))))))
3(1(1(z0))) → 3(1(4(1(z0))))
3(1(1(z0))) → 3(4(1(4(4(1(z0))))))
3(1(1(z0))) → 3(4(4(1(2(4(1(z0)))))))
3(3(1(z0))) → 3(2(1(3(z0))))
3(0(1(1(z0)))) → 0(2(1(3(1(z0)))))
3(1(1(5(z0)))) → 3(1(2(1(5(z0)))))
3(0(1(4(3(z0))))) → 3(2(0(3(4(1(z0))))))
3(0(4(5(1(z0))))) → 3(5(4(4(1(0(z0))))))
3(1(1(1(2(z0))))) → 3(2(1(4(1(2(1(2(z0))))))))
3(0(4(1(2(2(z0)))))) → 3(2(1(0(4(4(2(z0)))))))
3(1(0(3(5(4(z0)))))) → 3(0(3(2(1(5(4(z0)))))))
3(2(2(1(1(3(z0)))))) → 1(2(1(3(2(4(3(z0)))))))
3(3(3(1(3(5(z0)))))) → 3(2(1(3(3(3(5(z0)))))))
3(4(3(0(4(5(z0)))))) → 3(5(0(3(4(4(4(z0)))))))
3(4(3(1(4(2(z0)))))) → 3(4(2(1(3(2(2(4(2(4(z0))))))))))
3(5(0(2(1(4(z0)))))) → 3(2(4(0(5(1(2(z0)))))))
3(5(5(2(3(1(z0)))))) → 5(5(4(3(3(2(1(z0)))))))
3(2(5(0(4(0(1(z0))))))) → 0(0(5(4(2(2(4(4(1(3(z0))))))))))
3(4(3(4(0(1(4(z0))))))) → 3(4(2(4(4(4(0(5(1(2(3(z0)))))))))))
3(5(2(1(0(2(2(z0))))))) → 2(1(3(0(5(2(2(4(z0))))))))
3(5(2(2(0(1(1(z0))))))) → 3(2(4(5(0(2(1(2(1(z0)))))))))
3(5(3(4(0(1(4(z0))))))) → 2(1(5(4(3(4(0(3(z0))))))))
3(0(1(3(2(0(4(2(z0)))))))) → 0(4(2(2(2(4(1(0(3(3(4(z0)))))))))))
3(3(1(1(2(5(5(2(z0)))))))) → 3(2(1(5(1(2(5(3(1(z0)))))))))
3(5(4(2(5(1(0(4(z0)))))))) → 4(2(4(2(1(3(5(0(5(4(z0))))))))))
3(0(4(3(5(4(3(0(1(z0))))))))) → 0(3(0(3(4(3(2(4(5(1(z0))))))))))
3(1(5(3(1(1(0(3(2(z0))))))))) → 5(1(0(3(2(1(3(3(2(1(z0))))))))))
3(3(0(0(1(5(4(0(4(z0))))))))) → 1(0(2(4(4(0(3(5(0(3(z0))))))))))
3(2(0(2(0(5(2(3(4(5(z0)))))))))) → 3(5(4(4(2(0(3(2(5(2(0(z0)))))))))))
5(0(4(z0))) → 4(0(5(4(z0))))
5(0(1(5(z0)))) → 0(5(4(1(5(z0)))))
5(2(3(1(z0)))) → 4(5(2(1(3(z0)))))
5(2(3(5(z0)))) → 2(4(5(3(5(z0)))))
5(2(5(4(z0)))) → 2(4(5(4(5(z0)))))
5(2(3(1(4(z0))))) → 5(2(1(2(1(3(4(z0)))))))
5(3(0(0(4(z0))))) → 0(0(3(5(4(4(z0))))))
5(0(1(2(3(1(z0)))))) → 2(1(0(3(4(5(4(4(4(1(z0))))))))))
5(0(4(3(3(1(z0)))))) → 0(3(5(1(5(4(4(3(z0))))))))
5(1(5(3(1(1(3(z0))))))) → 2(1(5(1(5(1(3(3(z0))))))))
5(2(0(0(1(0(3(z0))))))) → 0(5(3(4(2(1(0(0(z0))))))))
5(2(0(4(0(4(3(z0))))))) → 2(0(5(1(0(4(4(3(z0))))))))
5(2(3(0(0(4(3(z0))))))) → 0(5(4(2(4(3(0(3(3(z0)))))))))
5(2(3(3(2(0(5(z0))))))) → 2(0(3(3(5(2(4(5(z0))))))))
5(5(5(0(1(4(3(z0))))))) → 0(5(4(4(3(4(5(5(1(z0)))))))))
5(0(4(3(0(2(2(3(z0)))))))) → 0(2(4(4(0(3(2(5(3(z0)))))))))
5(2(2(0(4(0(1(4(z0)))))))) → 4(2(4(0(0(5(1(0(2(z0)))))))))
5(2(2(0(4(1(5(4(z0)))))))) → 2(5(2(4(5(0(2(1(4(z0)))))))))
5(3(2(2(1(1(0(5(z0)))))))) → 0(3(2(5(2(1(5(1(2(z0)))))))))
5(2(0(3(1(2(5(0(4(z0))))))))) → 5(1(0(3(5(2(4(2(4(0(z0))))))))))
5(2(0(3(2(0(4(4(1(z0))))))))) → 0(5(3(0(5(2(2(4(2(4(1(z0)))))))))))
5(5(0(1(1(3(2(5(2(z0))))))))) → 3(5(1(2(2(0(5(1(5(4(z0))))))))))
5(5(3(2(1(0(1(0(4(z0))))))))) → 0(2(1(3(5(0(5(4(2(4(1(z0)))))))))))
Tuples:
0'(0(1(z0))) → c(0'(0(2(1(z0)))), 0'(2(1(z0))))
0'(1(3(z0))) → c1(0'(3(4(1(z0)))), 3'(4(1(z0))))
0'(0(0(1(z0)))) → c2(0'(0(0(2(1(z0))))), 0'(0(2(1(z0)))), 0'(2(1(z0))))
0'(0(1(5(z0)))) → c3(0'(0(5(1(2(4(z0)))))), 0'(5(1(2(4(z0))))), 5'(1(2(4(z0)))))
0'(0(5(3(z0)))) → c4(0'(0(5(4(3(z0))))), 0'(5(4(3(z0)))), 5'(4(3(z0))), 3'(z0))
0'(4(1(1(z0)))) → c5(0'(5(4(1(2(1(z0)))))), 5'(4(1(2(1(z0))))))
0'(4(3(1(z0)))) → c6(0'(3(5(4(1(z0))))), 3'(5(4(1(z0)))), 5'(4(1(z0))))
0'(4(3(4(z0)))) → c7(0'(3(2(4(4(z0))))), 3'(2(4(4(z0)))))
0'(1(2(2(1(z0))))) → c8(0'(1(2(1(z0)))))
0'(1(5(0(4(z0))))) → c9(0'(2(1(5(4(0(z0)))))), 5'(4(0(z0))), 0'(z0))
0'(1(5(5(3(z0))))) → c10(0'(5(4(5(1(3(z0)))))), 5'(4(5(1(3(z0))))), 5'(1(3(z0))), 3'(z0))
0'(2(2(1(5(z0))))) → c11(0'(2(1(5(4(2(4(4(2(z0))))))))), 5'(4(2(4(4(2(z0)))))))
0'(2(2(3(4(z0))))) → c12(0'(3(4(4(2(4(4(2(z0)))))))), 3'(4(4(2(4(4(2(z0))))))))
0'(2(5(1(1(z0))))) → c13(5'(0(1(2(4(1(z0)))))), 0'(1(2(4(1(z0))))))
0'(3(3(2(3(z0))))) → c14(0'(3(3(2(4(3(z0)))))), 3'(3(2(4(3(z0))))), 3'(2(4(3(z0)))), 3'(z0))
0'(4(4(3(4(z0))))) → c15(0'(3(z0)), 3'(z0))
0'(1(3(4(3(4(z0)))))) → c16(0'(3(4(3(4(1(2(z0))))))), 3'(4(3(4(1(2(z0)))))), 3'(4(1(2(z0)))))
0'(1(5(0(4(2(z0)))))) → c17(0'(5(2(4(1(0(2(z0))))))), 5'(2(4(1(0(2(z0)))))), 0'(2(z0)))
0'(2(2(2(3(1(z0)))))) → c18(0'(2(2(4(2(3(1(z0))))))), 3'(1(z0)))
0'(4(1(1(0(4(z0)))))) → c19(0'(4(4(1(4(1(0(z0))))))), 0'(z0))
0'(4(3(2(2(3(z0)))))) → c20(0'(2(3(2(4(2(3(z0))))))), 3'(2(4(2(3(z0))))), 3'(z0))
0'(0(1(1(3(3(3(z0))))))) → c21(0'(3(0(1(3(3(4(1(z0)))))))), 3'(0(1(3(3(4(1(z0))))))), 0'(1(3(3(4(1(z0)))))), 3'(3(4(1(z0)))), 3'(4(1(z0))))
0'(0(2(5(1(4(2(z0))))))) → c22(0'(2(1(0(5(4(2(2(z0)))))))), 0'(5(4(2(2(z0))))), 5'(4(2(2(z0)))))
0'(2(5(4(4(1(5(z0))))))) → c23(5'(0(5(4(4(z0))))), 0'(5(4(4(z0)))), 5'(4(4(z0))))
0'(4(2(3(4(5(4(z0))))))) → c24(3'(0(5(4(4(2(4(0(z0)))))))), 0'(5(4(4(2(4(0(z0))))))), 5'(4(4(2(4(0(z0)))))), 0'(z0))
0'(5(2(1(2(1(4(z0))))))) → c25(0'(5(2(4(z0)))), 5'(2(4(z0))))
0'(2(0(5(5(2(2(3(z0)))))))) → c26(5'(2(2(4(5(3(2(0(0(z0))))))))), 5'(3(2(0(0(z0))))), 3'(2(0(0(z0)))), 0'(0(z0)), 0'(z0))
0'(2(5(2(4(0(1(4(z0)))))))) → c27(0'(3(0(5(2(1(2(2(4(4(z0)))))))))), 3'(0(5(2(1(2(2(4(4(z0))))))))), 0'(5(2(1(2(2(4(4(z0)))))))), 5'(2(1(2(2(4(4(z0))))))))
0'(4(1(5(3(2(3(3(z0)))))))) → c28(0'(5(4(1(2(3(3(4(3(z0))))))))), 5'(4(1(2(3(3(4(3(z0)))))))), 3'(3(4(3(z0)))), 3'(4(3(z0))), 3'(z0))
0'(4(5(0(1(5(2(3(z0)))))))) → c29(5'(3(0(5(0(z0))))), 3'(0(5(0(z0)))), 0'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(5(5(1(4(2(0(3(z0)))))))) → c30(0'(3(5(1(2(0(5(1(2(4(z0)))))))))), 3'(5(1(2(0(5(1(2(4(z0))))))))), 5'(1(2(0(5(1(2(4(z0)))))))), 0'(5(1(2(4(z0))))), 5'(1(2(4(z0)))))
0'(0(4(4(5(3(1(1(5(z0))))))))) → c31(5'(4(4(4(1(0(0(3(5(z0))))))))), 0'(0(3(5(z0)))), 0'(3(5(z0))), 3'(5(z0)), 5'(z0))
0'(1(2(5(1(4(0(3(4(z0))))))))) → c32(0'(2(4(0(3(1(2(1(2(4(5(z0))))))))))), 0'(3(1(2(1(2(4(5(z0)))))))), 3'(1(2(1(2(4(5(z0))))))), 5'(z0))
0'(1(3(1(2(0(1(1(5(z0))))))))) → c33(0'(5(1(0(1(4(1(1(2(3(z0)))))))))), 5'(1(0(1(4(1(1(2(3(z0))))))))), 0'(1(4(1(1(2(3(z0))))))), 3'(z0))
0'(2(0(4(1(5(3(0(4(z0))))))))) → c34(0'(3(5(0(0(2(2(4(z0)))))))), 3'(5(0(0(2(2(4(z0))))))), 5'(0(0(2(2(4(z0)))))), 0'(0(2(2(4(z0))))), 0'(2(2(4(z0)))))
0'(4(3(3(4(2(5(0(5(z0))))))))) → c35(0'(5(0(4(3(2(4(5(3(2(z0)))))))))), 5'(0(4(3(2(4(5(3(2(z0))))))))), 0'(4(3(2(4(5(3(2(z0)))))))), 3'(2(4(5(3(2(z0)))))), 5'(3(2(z0))), 3'(2(z0)))
0'(1(3(1(4(2(0(4(5(2(z0)))))))))) → c36(0'(1(2(4(0(2(1(5(1(3(z0)))))))))), 0'(2(1(5(1(3(z0)))))), 5'(1(3(z0))), 3'(z0))
0'(4(3(1(3(5(2(5(4(4(z0)))))))))) → c37(0'(5(5(2(4(4(1(5(4(3(3(z0))))))))))), 5'(5(2(4(4(1(5(4(3(3(z0)))))))))), 5'(2(4(4(1(5(4(3(3(z0))))))))), 5'(4(3(3(z0)))), 3'(3(z0)), 3'(z0))
3'(1(1(z0))) → c38(3'(1(4(1(z0)))))
3'(1(1(z0))) → c39(3'(4(1(4(4(1(z0)))))))
3'(1(1(z0))) → c40(3'(4(4(1(2(4(1(z0))))))))
3'(3(1(z0))) → c41(3'(2(1(3(z0)))), 3'(z0))
3'(0(1(1(z0)))) → c42(0'(2(1(3(1(z0))))), 3'(1(z0)))
3'(1(1(5(z0)))) → c43(3'(1(2(1(5(z0))))), 5'(z0))
3'(0(1(4(3(z0))))) → c44(3'(2(0(3(4(1(z0)))))), 0'(3(4(1(z0)))), 3'(4(1(z0))))
3'(0(4(5(1(z0))))) → c45(3'(5(4(4(1(0(z0)))))), 5'(4(4(1(0(z0))))), 0'(z0))
3'(1(1(1(2(z0))))) → c46(3'(2(1(4(1(2(1(2(z0)))))))))
3'(0(4(1(2(2(z0)))))) → c47(3'(2(1(0(4(4(2(z0))))))), 0'(4(4(2(z0)))))
3'(1(0(3(5(4(z0)))))) → c48(3'(0(3(2(1(5(4(z0))))))), 0'(3(2(1(5(4(z0)))))), 3'(2(1(5(4(z0))))), 5'(4(z0)))
3'(2(2(1(1(3(z0)))))) → c49(3'(2(4(3(z0)))), 3'(z0))
3'(3(3(1(3(5(z0)))))) → c50(3'(2(1(3(3(3(5(z0))))))), 3'(3(3(5(z0)))), 3'(3(5(z0))), 3'(5(z0)), 5'(z0))
3'(4(3(0(4(5(z0)))))) → c51(3'(5(0(3(4(4(4(z0))))))), 5'(0(3(4(4(4(z0)))))), 0'(3(4(4(4(z0))))), 3'(4(4(4(z0)))))
3'(4(3(1(4(2(z0)))))) → c52(3'(4(2(1(3(2(2(4(2(4(z0)))))))))), 3'(2(2(4(2(4(z0)))))))
3'(5(0(2(1(4(z0)))))) → c53(3'(2(4(0(5(1(2(z0))))))), 0'(5(1(2(z0)))), 5'(1(2(z0))))
3'(5(5(2(3(1(z0)))))) → c54(5'(5(4(3(3(2(1(z0))))))), 5'(4(3(3(2(1(z0)))))), 3'(3(2(1(z0)))), 3'(2(1(z0))))
3'(2(5(0(4(0(1(z0))))))) → c55(0'(0(5(4(2(2(4(4(1(3(z0)))))))))), 0'(5(4(2(2(4(4(1(3(z0))))))))), 5'(4(2(2(4(4(1(3(z0)))))))), 3'(z0))
3'(4(3(4(0(1(4(z0))))))) → c56(3'(4(2(4(4(4(0(5(1(2(3(z0))))))))))), 0'(5(1(2(3(z0))))), 5'(1(2(3(z0)))), 3'(z0))
3'(5(2(1(0(2(2(z0))))))) → c57(3'(0(5(2(2(4(z0)))))), 0'(5(2(2(4(z0))))), 5'(2(2(4(z0)))))
3'(5(2(2(0(1(1(z0))))))) → c58(3'(2(4(5(0(2(1(2(1(z0))))))))), 5'(0(2(1(2(1(z0)))))), 0'(2(1(2(1(z0))))))
3'(5(3(4(0(1(4(z0))))))) → c59(5'(4(3(4(0(3(z0)))))), 3'(4(0(3(z0)))), 0'(3(z0)), 3'(z0))
3'(0(1(3(2(0(4(2(z0)))))))) → c60(0'(4(2(2(2(4(1(0(3(3(4(z0))))))))))), 0'(3(3(4(z0)))), 3'(3(4(z0))), 3'(4(z0)))
3'(3(1(1(2(5(5(2(z0)))))))) → c61(3'(2(1(5(1(2(5(3(1(z0))))))))), 5'(1(2(5(3(1(z0)))))), 5'(3(1(z0))), 3'(1(z0)))
3'(5(4(2(5(1(0(4(z0)))))))) → c62(3'(5(0(5(4(z0))))), 5'(0(5(4(z0)))), 0'(5(4(z0))), 5'(4(z0)))
3'(0(4(3(5(4(3(0(1(z0))))))))) → c63(0'(3(0(3(4(3(2(4(5(1(z0)))))))))), 3'(0(3(4(3(2(4(5(1(z0))))))))), 0'(3(4(3(2(4(5(1(z0)))))))), 3'(4(3(2(4(5(1(z0))))))), 3'(2(4(5(1(z0))))), 5'(1(z0)))
3'(1(5(3(1(1(0(3(2(z0))))))))) → c64(5'(1(0(3(2(1(3(3(2(1(z0)))))))))), 0'(3(2(1(3(3(2(1(z0)))))))), 3'(2(1(3(3(2(1(z0))))))), 3'(3(2(1(z0)))), 3'(2(1(z0))))
3'(3(0(0(1(5(4(0(4(z0))))))))) → c65(0'(2(4(4(0(3(5(0(3(z0))))))))), 0'(3(5(0(3(z0))))), 3'(5(0(3(z0)))), 5'(0(3(z0))), 0'(3(z0)), 3'(z0))
3'(2(0(2(0(5(2(3(4(5(z0)))))))))) → c66(3'(5(4(4(2(0(3(2(5(2(0(z0))))))))))), 5'(4(4(2(0(3(2(5(2(0(z0)))))))))), 0'(3(2(5(2(0(z0)))))), 3'(2(5(2(0(z0))))), 5'(2(0(z0))), 0'(z0))
5'(0(4(z0))) → c67(0'(5(4(z0))), 5'(4(z0)))
5'(0(1(5(z0)))) → c68(0'(5(4(1(5(z0))))), 5'(4(1(5(z0)))), 5'(z0))
5'(2(3(1(z0)))) → c69(5'(2(1(3(z0)))), 3'(z0))
5'(2(3(5(z0)))) → c70(5'(3(5(z0))), 3'(5(z0)), 5'(z0))
5'(2(5(4(z0)))) → c71(5'(4(5(z0))), 5'(z0))
5'(2(3(1(4(z0))))) → c72(5'(2(1(2(1(3(4(z0))))))), 3'(4(z0)))
5'(3(0(0(4(z0))))) → c73(0'(0(3(5(4(4(z0)))))), 0'(3(5(4(4(z0))))), 3'(5(4(4(z0)))), 5'(4(4(z0))))
5'(0(1(2(3(1(z0)))))) → c74(0'(3(4(5(4(4(4(1(z0)))))))), 3'(4(5(4(4(4(1(z0))))))), 5'(4(4(4(1(z0))))))
5'(0(4(3(3(1(z0)))))) → c75(0'(3(5(1(5(4(4(3(z0)))))))), 3'(5(1(5(4(4(3(z0))))))), 5'(1(5(4(4(3(z0)))))), 5'(4(4(3(z0)))), 3'(z0))
5'(1(5(3(1(1(3(z0))))))) → c76(5'(1(5(1(3(3(z0)))))), 5'(1(3(3(z0)))), 3'(3(z0)), 3'(z0))
5'(2(0(0(1(0(3(z0))))))) → c77(0'(5(3(4(2(1(0(0(z0)))))))), 5'(3(4(2(1(0(0(z0))))))), 3'(4(2(1(0(0(z0)))))), 0'(0(z0)), 0'(z0))
5'(2(0(4(0(4(3(z0))))))) → c78(0'(5(1(0(4(4(3(z0))))))), 5'(1(0(4(4(3(z0)))))), 0'(4(4(3(z0)))), 3'(z0))
5'(2(3(0(0(4(3(z0))))))) → c79(0'(5(4(2(4(3(0(3(3(z0))))))))), 5'(4(2(4(3(0(3(3(z0)))))))), 3'(0(3(3(z0)))), 0'(3(3(z0))), 3'(3(z0)), 3'(z0))
5'(2(3(3(2(0(5(z0))))))) → c80(0'(3(3(5(2(4(5(z0))))))), 3'(3(5(2(4(5(z0)))))), 3'(5(2(4(5(z0))))), 5'(2(4(5(z0)))), 5'(z0))
5'(5(5(0(1(4(3(z0))))))) → c81(0'(5(4(4(3(4(5(5(1(z0))))))))), 5'(4(4(3(4(5(5(1(z0)))))))), 3'(4(5(5(1(z0))))), 5'(5(1(z0))), 5'(1(z0)))
5'(0(4(3(0(2(2(3(z0)))))))) → c82(0'(2(4(4(0(3(2(5(3(z0))))))))), 0'(3(2(5(3(z0))))), 3'(2(5(3(z0)))), 5'(3(z0)), 3'(z0))
5'(2(2(0(4(0(1(4(z0)))))))) → c83(0'(0(5(1(0(2(z0)))))), 0'(5(1(0(2(z0))))), 5'(1(0(2(z0)))), 0'(2(z0)))
5'(2(2(0(4(1(5(4(z0)))))))) → c84(5'(2(4(5(0(2(1(4(z0)))))))), 5'(0(2(1(4(z0))))), 0'(2(1(4(z0)))))
5'(3(2(2(1(1(0(5(z0)))))))) → c85(0'(3(2(5(2(1(5(1(2(z0))))))))), 3'(2(5(2(1(5(1(2(z0)))))))), 5'(2(1(5(1(2(z0)))))), 5'(1(2(z0))))
5'(2(0(3(1(2(5(0(4(z0))))))))) → c86(5'(1(0(3(5(2(4(2(4(0(z0)))))))))), 0'(3(5(2(4(2(4(0(z0)))))))), 3'(5(2(4(2(4(0(z0))))))), 5'(2(4(2(4(0(z0)))))), 0'(z0))
5'(2(0(3(2(0(4(4(1(z0))))))))) → c87(0'(5(3(0(5(2(2(4(2(4(1(z0))))))))))), 5'(3(0(5(2(2(4(2(4(1(z0)))))))))), 3'(0(5(2(2(4(2(4(1(z0))))))))), 0'(5(2(2(4(2(4(1(z0)))))))), 5'(2(2(4(2(4(1(z0))))))))
5'(5(0(1(1(3(2(5(2(z0))))))))) → c88(3'(5(1(2(2(0(5(1(5(4(z0)))))))))), 5'(1(2(2(0(5(1(5(4(z0))))))))), 0'(5(1(5(4(z0))))), 5'(1(5(4(z0)))), 5'(4(z0)))
5'(5(3(2(1(0(1(0(4(z0))))))))) → c89(0'(2(1(3(5(0(5(4(2(4(1(z0))))))))))), 3'(5(0(5(4(2(4(1(z0)))))))), 5'(0(5(4(2(4(1(z0))))))), 0'(5(4(2(4(1(z0)))))), 5'(4(2(4(1(z0))))))
S tuples:
0'(0(1(z0))) → c(0'(0(2(1(z0)))), 0'(2(1(z0))))
0'(1(3(z0))) → c1(0'(3(4(1(z0)))), 3'(4(1(z0))))
0'(0(0(1(z0)))) → c2(0'(0(0(2(1(z0))))), 0'(0(2(1(z0)))), 0'(2(1(z0))))
0'(0(1(5(z0)))) → c3(0'(0(5(1(2(4(z0)))))), 0'(5(1(2(4(z0))))), 5'(1(2(4(z0)))))
0'(0(5(3(z0)))) → c4(0'(0(5(4(3(z0))))), 0'(5(4(3(z0)))), 5'(4(3(z0))), 3'(z0))
0'(4(1(1(z0)))) → c5(0'(5(4(1(2(1(z0)))))), 5'(4(1(2(1(z0))))))
0'(4(3(1(z0)))) → c6(0'(3(5(4(1(z0))))), 3'(5(4(1(z0)))), 5'(4(1(z0))))
0'(4(3(4(z0)))) → c7(0'(3(2(4(4(z0))))), 3'(2(4(4(z0)))))
0'(1(2(2(1(z0))))) → c8(0'(1(2(1(z0)))))
0'(1(5(0(4(z0))))) → c9(0'(2(1(5(4(0(z0)))))), 5'(4(0(z0))), 0'(z0))
0'(1(5(5(3(z0))))) → c10(0'(5(4(5(1(3(z0)))))), 5'(4(5(1(3(z0))))), 5'(1(3(z0))), 3'(z0))
0'(2(2(1(5(z0))))) → c11(0'(2(1(5(4(2(4(4(2(z0))))))))), 5'(4(2(4(4(2(z0)))))))
0'(2(2(3(4(z0))))) → c12(0'(3(4(4(2(4(4(2(z0)))))))), 3'(4(4(2(4(4(2(z0))))))))
0'(2(5(1(1(z0))))) → c13(5'(0(1(2(4(1(z0)))))), 0'(1(2(4(1(z0))))))
0'(3(3(2(3(z0))))) → c14(0'(3(3(2(4(3(z0)))))), 3'(3(2(4(3(z0))))), 3'(2(4(3(z0)))), 3'(z0))
0'(4(4(3(4(z0))))) → c15(0'(3(z0)), 3'(z0))
0'(1(3(4(3(4(z0)))))) → c16(0'(3(4(3(4(1(2(z0))))))), 3'(4(3(4(1(2(z0)))))), 3'(4(1(2(z0)))))
0'(1(5(0(4(2(z0)))))) → c17(0'(5(2(4(1(0(2(z0))))))), 5'(2(4(1(0(2(z0)))))), 0'(2(z0)))
0'(2(2(2(3(1(z0)))))) → c18(0'(2(2(4(2(3(1(z0))))))), 3'(1(z0)))
0'(4(1(1(0(4(z0)))))) → c19(0'(4(4(1(4(1(0(z0))))))), 0'(z0))
0'(4(3(2(2(3(z0)))))) → c20(0'(2(3(2(4(2(3(z0))))))), 3'(2(4(2(3(z0))))), 3'(z0))
0'(0(1(1(3(3(3(z0))))))) → c21(0'(3(0(1(3(3(4(1(z0)))))))), 3'(0(1(3(3(4(1(z0))))))), 0'(1(3(3(4(1(z0)))))), 3'(3(4(1(z0)))), 3'(4(1(z0))))
0'(0(2(5(1(4(2(z0))))))) → c22(0'(2(1(0(5(4(2(2(z0)))))))), 0'(5(4(2(2(z0))))), 5'(4(2(2(z0)))))
0'(2(5(4(4(1(5(z0))))))) → c23(5'(0(5(4(4(z0))))), 0'(5(4(4(z0)))), 5'(4(4(z0))))
0'(4(2(3(4(5(4(z0))))))) → c24(3'(0(5(4(4(2(4(0(z0)))))))), 0'(5(4(4(2(4(0(z0))))))), 5'(4(4(2(4(0(z0)))))), 0'(z0))
0'(5(2(1(2(1(4(z0))))))) → c25(0'(5(2(4(z0)))), 5'(2(4(z0))))
0'(2(0(5(5(2(2(3(z0)))))))) → c26(5'(2(2(4(5(3(2(0(0(z0))))))))), 5'(3(2(0(0(z0))))), 3'(2(0(0(z0)))), 0'(0(z0)), 0'(z0))
0'(2(5(2(4(0(1(4(z0)))))))) → c27(0'(3(0(5(2(1(2(2(4(4(z0)))))))))), 3'(0(5(2(1(2(2(4(4(z0))))))))), 0'(5(2(1(2(2(4(4(z0)))))))), 5'(2(1(2(2(4(4(z0))))))))
0'(4(1(5(3(2(3(3(z0)))))))) → c28(0'(5(4(1(2(3(3(4(3(z0))))))))), 5'(4(1(2(3(3(4(3(z0)))))))), 3'(3(4(3(z0)))), 3'(4(3(z0))), 3'(z0))
0'(4(5(0(1(5(2(3(z0)))))))) → c29(5'(3(0(5(0(z0))))), 3'(0(5(0(z0)))), 0'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(5(5(1(4(2(0(3(z0)))))))) → c30(0'(3(5(1(2(0(5(1(2(4(z0)))))))))), 3'(5(1(2(0(5(1(2(4(z0))))))))), 5'(1(2(0(5(1(2(4(z0)))))))), 0'(5(1(2(4(z0))))), 5'(1(2(4(z0)))))
0'(0(4(4(5(3(1(1(5(z0))))))))) → c31(5'(4(4(4(1(0(0(3(5(z0))))))))), 0'(0(3(5(z0)))), 0'(3(5(z0))), 3'(5(z0)), 5'(z0))
0'(1(2(5(1(4(0(3(4(z0))))))))) → c32(0'(2(4(0(3(1(2(1(2(4(5(z0))))))))))), 0'(3(1(2(1(2(4(5(z0)))))))), 3'(1(2(1(2(4(5(z0))))))), 5'(z0))
0'(1(3(1(2(0(1(1(5(z0))))))))) → c33(0'(5(1(0(1(4(1(1(2(3(z0)))))))))), 5'(1(0(1(4(1(1(2(3(z0))))))))), 0'(1(4(1(1(2(3(z0))))))), 3'(z0))
0'(2(0(4(1(5(3(0(4(z0))))))))) → c34(0'(3(5(0(0(2(2(4(z0)))))))), 3'(5(0(0(2(2(4(z0))))))), 5'(0(0(2(2(4(z0)))))), 0'(0(2(2(4(z0))))), 0'(2(2(4(z0)))))
0'(4(3(3(4(2(5(0(5(z0))))))))) → c35(0'(5(0(4(3(2(4(5(3(2(z0)))))))))), 5'(0(4(3(2(4(5(3(2(z0))))))))), 0'(4(3(2(4(5(3(2(z0)))))))), 3'(2(4(5(3(2(z0)))))), 5'(3(2(z0))), 3'(2(z0)))
0'(1(3(1(4(2(0(4(5(2(z0)))))))))) → c36(0'(1(2(4(0(2(1(5(1(3(z0)))))))))), 0'(2(1(5(1(3(z0)))))), 5'(1(3(z0))), 3'(z0))
0'(4(3(1(3(5(2(5(4(4(z0)))))))))) → c37(0'(5(5(2(4(4(1(5(4(3(3(z0))))))))))), 5'(5(2(4(4(1(5(4(3(3(z0)))))))))), 5'(2(4(4(1(5(4(3(3(z0))))))))), 5'(4(3(3(z0)))), 3'(3(z0)), 3'(z0))
3'(1(1(z0))) → c38(3'(1(4(1(z0)))))
3'(1(1(z0))) → c39(3'(4(1(4(4(1(z0)))))))
3'(1(1(z0))) → c40(3'(4(4(1(2(4(1(z0))))))))
3'(3(1(z0))) → c41(3'(2(1(3(z0)))), 3'(z0))
3'(0(1(1(z0)))) → c42(0'(2(1(3(1(z0))))), 3'(1(z0)))
3'(1(1(5(z0)))) → c43(3'(1(2(1(5(z0))))), 5'(z0))
3'(0(1(4(3(z0))))) → c44(3'(2(0(3(4(1(z0)))))), 0'(3(4(1(z0)))), 3'(4(1(z0))))
3'(0(4(5(1(z0))))) → c45(3'(5(4(4(1(0(z0)))))), 5'(4(4(1(0(z0))))), 0'(z0))
3'(1(1(1(2(z0))))) → c46(3'(2(1(4(1(2(1(2(z0)))))))))
3'(0(4(1(2(2(z0)))))) → c47(3'(2(1(0(4(4(2(z0))))))), 0'(4(4(2(z0)))))
3'(1(0(3(5(4(z0)))))) → c48(3'(0(3(2(1(5(4(z0))))))), 0'(3(2(1(5(4(z0)))))), 3'(2(1(5(4(z0))))), 5'(4(z0)))
3'(2(2(1(1(3(z0)))))) → c49(3'(2(4(3(z0)))), 3'(z0))
3'(3(3(1(3(5(z0)))))) → c50(3'(2(1(3(3(3(5(z0))))))), 3'(3(3(5(z0)))), 3'(3(5(z0))), 3'(5(z0)), 5'(z0))
3'(4(3(0(4(5(z0)))))) → c51(3'(5(0(3(4(4(4(z0))))))), 5'(0(3(4(4(4(z0)))))), 0'(3(4(4(4(z0))))), 3'(4(4(4(z0)))))
3'(4(3(1(4(2(z0)))))) → c52(3'(4(2(1(3(2(2(4(2(4(z0)))))))))), 3'(2(2(4(2(4(z0)))))))
3'(5(0(2(1(4(z0)))))) → c53(3'(2(4(0(5(1(2(z0))))))), 0'(5(1(2(z0)))), 5'(1(2(z0))))
3'(5(5(2(3(1(z0)))))) → c54(5'(5(4(3(3(2(1(z0))))))), 5'(4(3(3(2(1(z0)))))), 3'(3(2(1(z0)))), 3'(2(1(z0))))
3'(2(5(0(4(0(1(z0))))))) → c55(0'(0(5(4(2(2(4(4(1(3(z0)))))))))), 0'(5(4(2(2(4(4(1(3(z0))))))))), 5'(4(2(2(4(4(1(3(z0)))))))), 3'(z0))
3'(4(3(4(0(1(4(z0))))))) → c56(3'(4(2(4(4(4(0(5(1(2(3(z0))))))))))), 0'(5(1(2(3(z0))))), 5'(1(2(3(z0)))), 3'(z0))
3'(5(2(1(0(2(2(z0))))))) → c57(3'(0(5(2(2(4(z0)))))), 0'(5(2(2(4(z0))))), 5'(2(2(4(z0)))))
3'(5(2(2(0(1(1(z0))))))) → c58(3'(2(4(5(0(2(1(2(1(z0))))))))), 5'(0(2(1(2(1(z0)))))), 0'(2(1(2(1(z0))))))
3'(5(3(4(0(1(4(z0))))))) → c59(5'(4(3(4(0(3(z0)))))), 3'(4(0(3(z0)))), 0'(3(z0)), 3'(z0))
3'(0(1(3(2(0(4(2(z0)))))))) → c60(0'(4(2(2(2(4(1(0(3(3(4(z0))))))))))), 0'(3(3(4(z0)))), 3'(3(4(z0))), 3'(4(z0)))
3'(3(1(1(2(5(5(2(z0)))))))) → c61(3'(2(1(5(1(2(5(3(1(z0))))))))), 5'(1(2(5(3(1(z0)))))), 5'(3(1(z0))), 3'(1(z0)))
3'(5(4(2(5(1(0(4(z0)))))))) → c62(3'(5(0(5(4(z0))))), 5'(0(5(4(z0)))), 0'(5(4(z0))), 5'(4(z0)))
3'(0(4(3(5(4(3(0(1(z0))))))))) → c63(0'(3(0(3(4(3(2(4(5(1(z0)))))))))), 3'(0(3(4(3(2(4(5(1(z0))))))))), 0'(3(4(3(2(4(5(1(z0)))))))), 3'(4(3(2(4(5(1(z0))))))), 3'(2(4(5(1(z0))))), 5'(1(z0)))
3'(1(5(3(1(1(0(3(2(z0))))))))) → c64(5'(1(0(3(2(1(3(3(2(1(z0)))))))))), 0'(3(2(1(3(3(2(1(z0)))))))), 3'(2(1(3(3(2(1(z0))))))), 3'(3(2(1(z0)))), 3'(2(1(z0))))
3'(3(0(0(1(5(4(0(4(z0))))))))) → c65(0'(2(4(4(0(3(5(0(3(z0))))))))), 0'(3(5(0(3(z0))))), 3'(5(0(3(z0)))), 5'(0(3(z0))), 0'(3(z0)), 3'(z0))
3'(2(0(2(0(5(2(3(4(5(z0)))))))))) → c66(3'(5(4(4(2(0(3(2(5(2(0(z0))))))))))), 5'(4(4(2(0(3(2(5(2(0(z0)))))))))), 0'(3(2(5(2(0(z0)))))), 3'(2(5(2(0(z0))))), 5'(2(0(z0))), 0'(z0))
5'(0(4(z0))) → c67(0'(5(4(z0))), 5'(4(z0)))
5'(0(1(5(z0)))) → c68(0'(5(4(1(5(z0))))), 5'(4(1(5(z0)))), 5'(z0))
5'(2(3(1(z0)))) → c69(5'(2(1(3(z0)))), 3'(z0))
5'(2(3(5(z0)))) → c70(5'(3(5(z0))), 3'(5(z0)), 5'(z0))
5'(2(5(4(z0)))) → c71(5'(4(5(z0))), 5'(z0))
5'(2(3(1(4(z0))))) → c72(5'(2(1(2(1(3(4(z0))))))), 3'(4(z0)))
5'(3(0(0(4(z0))))) → c73(0'(0(3(5(4(4(z0)))))), 0'(3(5(4(4(z0))))), 3'(5(4(4(z0)))), 5'(4(4(z0))))
5'(0(1(2(3(1(z0)))))) → c74(0'(3(4(5(4(4(4(1(z0)))))))), 3'(4(5(4(4(4(1(z0))))))), 5'(4(4(4(1(z0))))))
5'(0(4(3(3(1(z0)))))) → c75(0'(3(5(1(5(4(4(3(z0)))))))), 3'(5(1(5(4(4(3(z0))))))), 5'(1(5(4(4(3(z0)))))), 5'(4(4(3(z0)))), 3'(z0))
5'(1(5(3(1(1(3(z0))))))) → c76(5'(1(5(1(3(3(z0)))))), 5'(1(3(3(z0)))), 3'(3(z0)), 3'(z0))
5'(2(0(0(1(0(3(z0))))))) → c77(0'(5(3(4(2(1(0(0(z0)))))))), 5'(3(4(2(1(0(0(z0))))))), 3'(4(2(1(0(0(z0)))))), 0'(0(z0)), 0'(z0))
5'(2(0(4(0(4(3(z0))))))) → c78(0'(5(1(0(4(4(3(z0))))))), 5'(1(0(4(4(3(z0)))))), 0'(4(4(3(z0)))), 3'(z0))
5'(2(3(0(0(4(3(z0))))))) → c79(0'(5(4(2(4(3(0(3(3(z0))))))))), 5'(4(2(4(3(0(3(3(z0)))))))), 3'(0(3(3(z0)))), 0'(3(3(z0))), 3'(3(z0)), 3'(z0))
5'(2(3(3(2(0(5(z0))))))) → c80(0'(3(3(5(2(4(5(z0))))))), 3'(3(5(2(4(5(z0)))))), 3'(5(2(4(5(z0))))), 5'(2(4(5(z0)))), 5'(z0))
5'(5(5(0(1(4(3(z0))))))) → c81(0'(5(4(4(3(4(5(5(1(z0))))))))), 5'(4(4(3(4(5(5(1(z0)))))))), 3'(4(5(5(1(z0))))), 5'(5(1(z0))), 5'(1(z0)))
5'(0(4(3(0(2(2(3(z0)))))))) → c82(0'(2(4(4(0(3(2(5(3(z0))))))))), 0'(3(2(5(3(z0))))), 3'(2(5(3(z0)))), 5'(3(z0)), 3'(z0))
5'(2(2(0(4(0(1(4(z0)))))))) → c83(0'(0(5(1(0(2(z0)))))), 0'(5(1(0(2(z0))))), 5'(1(0(2(z0)))), 0'(2(z0)))
5'(2(2(0(4(1(5(4(z0)))))))) → c84(5'(2(4(5(0(2(1(4(z0)))))))), 5'(0(2(1(4(z0))))), 0'(2(1(4(z0)))))
5'(3(2(2(1(1(0(5(z0)))))))) → c85(0'(3(2(5(2(1(5(1(2(z0))))))))), 3'(2(5(2(1(5(1(2(z0)))))))), 5'(2(1(5(1(2(z0)))))), 5'(1(2(z0))))
5'(2(0(3(1(2(5(0(4(z0))))))))) → c86(5'(1(0(3(5(2(4(2(4(0(z0)))))))))), 0'(3(5(2(4(2(4(0(z0)))))))), 3'(5(2(4(2(4(0(z0))))))), 5'(2(4(2(4(0(z0)))))), 0'(z0))
5'(2(0(3(2(0(4(4(1(z0))))))))) → c87(0'(5(3(0(5(2(2(4(2(4(1(z0))))))))))), 5'(3(0(5(2(2(4(2(4(1(z0)))))))))), 3'(0(5(2(2(4(2(4(1(z0))))))))), 0'(5(2(2(4(2(4(1(z0)))))))), 5'(2(2(4(2(4(1(z0))))))))
5'(5(0(1(1(3(2(5(2(z0))))))))) → c88(3'(5(1(2(2(0(5(1(5(4(z0)))))))))), 5'(1(2(2(0(5(1(5(4(z0))))))))), 0'(5(1(5(4(z0))))), 5'(1(5(4(z0)))), 5'(4(z0)))
5'(5(3(2(1(0(1(0(4(z0))))))))) → c89(0'(2(1(3(5(0(5(4(2(4(1(z0))))))))))), 3'(5(0(5(4(2(4(1(z0)))))))), 5'(0(5(4(2(4(1(z0))))))), 0'(5(4(2(4(1(z0)))))), 5'(4(2(4(1(z0))))))
K tuples:none
Defined Rule Symbols:
0, 3, 5
Defined Pair Symbols:
0', 3', 5'
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c67, c68, c69, c70, c71, c72, c73, c74, c75, c76, c77, c78, c79, c80, c81, c82, c83, c84, c85, c86, c87, c88, c89
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
0'(0(1(z0))) → c(0'(0(2(1(z0)))), 0'(2(1(z0))))
0'(1(3(z0))) → c1(0'(3(4(1(z0)))), 3'(4(1(z0))))
0'(0(0(1(z0)))) → c2(0'(0(0(2(1(z0))))), 0'(0(2(1(z0)))), 0'(2(1(z0))))
0'(0(1(5(z0)))) → c3(0'(0(5(1(2(4(z0)))))), 0'(5(1(2(4(z0))))), 5'(1(2(4(z0)))))
0'(0(5(3(z0)))) → c4(0'(0(5(4(3(z0))))), 0'(5(4(3(z0)))), 5'(4(3(z0))), 3'(z0))
0'(4(3(1(z0)))) → c6(0'(3(5(4(1(z0))))), 3'(5(4(1(z0)))), 5'(4(1(z0))))
0'(4(3(4(z0)))) → c7(0'(3(2(4(4(z0))))), 3'(2(4(4(z0)))))
0'(1(5(0(4(z0))))) → c9(0'(2(1(5(4(0(z0)))))), 5'(4(0(z0))), 0'(z0))
0'(1(5(5(3(z0))))) → c10(0'(5(4(5(1(3(z0)))))), 5'(4(5(1(3(z0))))), 5'(1(3(z0))), 3'(z0))
0'(2(2(1(5(z0))))) → c11(0'(2(1(5(4(2(4(4(2(z0))))))))), 5'(4(2(4(4(2(z0)))))))
0'(2(2(3(4(z0))))) → c12(0'(3(4(4(2(4(4(2(z0)))))))), 3'(4(4(2(4(4(2(z0))))))))
0'(2(5(1(1(z0))))) → c13(5'(0(1(2(4(1(z0)))))), 0'(1(2(4(1(z0))))))
0'(3(3(2(3(z0))))) → c14(0'(3(3(2(4(3(z0)))))), 3'(3(2(4(3(z0))))), 3'(2(4(3(z0)))), 3'(z0))
0'(4(4(3(4(z0))))) → c15(0'(3(z0)), 3'(z0))
0'(1(3(4(3(4(z0)))))) → c16(0'(3(4(3(4(1(2(z0))))))), 3'(4(3(4(1(2(z0)))))), 3'(4(1(2(z0)))))
0'(1(5(0(4(2(z0)))))) → c17(0'(5(2(4(1(0(2(z0))))))), 5'(2(4(1(0(2(z0)))))), 0'(2(z0)))
0'(2(2(2(3(1(z0)))))) → c18(0'(2(2(4(2(3(1(z0))))))), 3'(1(z0)))
0'(4(1(1(0(4(z0)))))) → c19(0'(4(4(1(4(1(0(z0))))))), 0'(z0))
0'(4(3(2(2(3(z0)))))) → c20(0'(2(3(2(4(2(3(z0))))))), 3'(2(4(2(3(z0))))), 3'(z0))
0'(0(1(1(3(3(3(z0))))))) → c21(0'(3(0(1(3(3(4(1(z0)))))))), 3'(0(1(3(3(4(1(z0))))))), 0'(1(3(3(4(1(z0)))))), 3'(3(4(1(z0)))), 3'(4(1(z0))))
0'(0(2(5(1(4(2(z0))))))) → c22(0'(2(1(0(5(4(2(2(z0)))))))), 0'(5(4(2(2(z0))))), 5'(4(2(2(z0)))))
0'(2(5(4(4(1(5(z0))))))) → c23(5'(0(5(4(4(z0))))), 0'(5(4(4(z0)))), 5'(4(4(z0))))
0'(4(2(3(4(5(4(z0))))))) → c24(3'(0(5(4(4(2(4(0(z0)))))))), 0'(5(4(4(2(4(0(z0))))))), 5'(4(4(2(4(0(z0)))))), 0'(z0))
0'(5(2(1(2(1(4(z0))))))) → c25(0'(5(2(4(z0)))), 5'(2(4(z0))))
0'(2(0(5(5(2(2(3(z0)))))))) → c26(5'(2(2(4(5(3(2(0(0(z0))))))))), 5'(3(2(0(0(z0))))), 3'(2(0(0(z0)))), 0'(0(z0)), 0'(z0))
0'(2(5(2(4(0(1(4(z0)))))))) → c27(0'(3(0(5(2(1(2(2(4(4(z0)))))))))), 3'(0(5(2(1(2(2(4(4(z0))))))))), 0'(5(2(1(2(2(4(4(z0)))))))), 5'(2(1(2(2(4(4(z0))))))))
0'(4(1(5(3(2(3(3(z0)))))))) → c28(0'(5(4(1(2(3(3(4(3(z0))))))))), 5'(4(1(2(3(3(4(3(z0)))))))), 3'(3(4(3(z0)))), 3'(4(3(z0))), 3'(z0))
0'(4(5(0(1(5(2(3(z0)))))))) → c29(5'(3(0(5(0(z0))))), 3'(0(5(0(z0)))), 0'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(5(5(1(4(2(0(3(z0)))))))) → c30(0'(3(5(1(2(0(5(1(2(4(z0)))))))))), 3'(5(1(2(0(5(1(2(4(z0))))))))), 5'(1(2(0(5(1(2(4(z0)))))))), 0'(5(1(2(4(z0))))), 5'(1(2(4(z0)))))
0'(0(4(4(5(3(1(1(5(z0))))))))) → c31(5'(4(4(4(1(0(0(3(5(z0))))))))), 0'(0(3(5(z0)))), 0'(3(5(z0))), 3'(5(z0)), 5'(z0))
0'(1(2(5(1(4(0(3(4(z0))))))))) → c32(0'(2(4(0(3(1(2(1(2(4(5(z0))))))))))), 0'(3(1(2(1(2(4(5(z0)))))))), 3'(1(2(1(2(4(5(z0))))))), 5'(z0))
0'(1(3(1(2(0(1(1(5(z0))))))))) → c33(0'(5(1(0(1(4(1(1(2(3(z0)))))))))), 5'(1(0(1(4(1(1(2(3(z0))))))))), 0'(1(4(1(1(2(3(z0))))))), 3'(z0))
0'(2(0(4(1(5(3(0(4(z0))))))))) → c34(0'(3(5(0(0(2(2(4(z0)))))))), 3'(5(0(0(2(2(4(z0))))))), 5'(0(0(2(2(4(z0)))))), 0'(0(2(2(4(z0))))), 0'(2(2(4(z0)))))
0'(4(3(3(4(2(5(0(5(z0))))))))) → c35(0'(5(0(4(3(2(4(5(3(2(z0)))))))))), 5'(0(4(3(2(4(5(3(2(z0))))))))), 0'(4(3(2(4(5(3(2(z0)))))))), 3'(2(4(5(3(2(z0)))))), 5'(3(2(z0))), 3'(2(z0)))
0'(1(3(1(4(2(0(4(5(2(z0)))))))))) → c36(0'(1(2(4(0(2(1(5(1(3(z0)))))))))), 0'(2(1(5(1(3(z0)))))), 5'(1(3(z0))), 3'(z0))
0'(4(3(1(3(5(2(5(4(4(z0)))))))))) → c37(0'(5(5(2(4(4(1(5(4(3(3(z0))))))))))), 5'(5(2(4(4(1(5(4(3(3(z0)))))))))), 5'(2(4(4(1(5(4(3(3(z0))))))))), 5'(4(3(3(z0)))), 3'(3(z0)), 3'(z0))
3'(3(1(z0))) → c41(3'(2(1(3(z0)))), 3'(z0))
3'(0(1(1(z0)))) → c42(0'(2(1(3(1(z0))))), 3'(1(z0)))
3'(1(1(5(z0)))) → c43(3'(1(2(1(5(z0))))), 5'(z0))
3'(0(1(4(3(z0))))) → c44(3'(2(0(3(4(1(z0)))))), 0'(3(4(1(z0)))), 3'(4(1(z0))))
3'(0(4(5(1(z0))))) → c45(3'(5(4(4(1(0(z0)))))), 5'(4(4(1(0(z0))))), 0'(z0))
3'(0(4(1(2(2(z0)))))) → c47(3'(2(1(0(4(4(2(z0))))))), 0'(4(4(2(z0)))))
3'(1(0(3(5(4(z0)))))) → c48(3'(0(3(2(1(5(4(z0))))))), 0'(3(2(1(5(4(z0)))))), 3'(2(1(5(4(z0))))), 5'(4(z0)))
3'(2(2(1(1(3(z0)))))) → c49(3'(2(4(3(z0)))), 3'(z0))
3'(3(3(1(3(5(z0)))))) → c50(3'(2(1(3(3(3(5(z0))))))), 3'(3(3(5(z0)))), 3'(3(5(z0))), 3'(5(z0)), 5'(z0))
3'(4(3(0(4(5(z0)))))) → c51(3'(5(0(3(4(4(4(z0))))))), 5'(0(3(4(4(4(z0)))))), 0'(3(4(4(4(z0))))), 3'(4(4(4(z0)))))
3'(4(3(1(4(2(z0)))))) → c52(3'(4(2(1(3(2(2(4(2(4(z0)))))))))), 3'(2(2(4(2(4(z0)))))))
3'(5(0(2(1(4(z0)))))) → c53(3'(2(4(0(5(1(2(z0))))))), 0'(5(1(2(z0)))), 5'(1(2(z0))))
3'(5(5(2(3(1(z0)))))) → c54(5'(5(4(3(3(2(1(z0))))))), 5'(4(3(3(2(1(z0)))))), 3'(3(2(1(z0)))), 3'(2(1(z0))))
3'(2(5(0(4(0(1(z0))))))) → c55(0'(0(5(4(2(2(4(4(1(3(z0)))))))))), 0'(5(4(2(2(4(4(1(3(z0))))))))), 5'(4(2(2(4(4(1(3(z0)))))))), 3'(z0))
3'(4(3(4(0(1(4(z0))))))) → c56(3'(4(2(4(4(4(0(5(1(2(3(z0))))))))))), 0'(5(1(2(3(z0))))), 5'(1(2(3(z0)))), 3'(z0))
3'(5(2(1(0(2(2(z0))))))) → c57(3'(0(5(2(2(4(z0)))))), 0'(5(2(2(4(z0))))), 5'(2(2(4(z0)))))
3'(5(2(2(0(1(1(z0))))))) → c58(3'(2(4(5(0(2(1(2(1(z0))))))))), 5'(0(2(1(2(1(z0)))))), 0'(2(1(2(1(z0))))))
3'(5(3(4(0(1(4(z0))))))) → c59(5'(4(3(4(0(3(z0)))))), 3'(4(0(3(z0)))), 0'(3(z0)), 3'(z0))
3'(0(1(3(2(0(4(2(z0)))))))) → c60(0'(4(2(2(2(4(1(0(3(3(4(z0))))))))))), 0'(3(3(4(z0)))), 3'(3(4(z0))), 3'(4(z0)))
3'(3(1(1(2(5(5(2(z0)))))))) → c61(3'(2(1(5(1(2(5(3(1(z0))))))))), 5'(1(2(5(3(1(z0)))))), 5'(3(1(z0))), 3'(1(z0)))
3'(5(4(2(5(1(0(4(z0)))))))) → c62(3'(5(0(5(4(z0))))), 5'(0(5(4(z0)))), 0'(5(4(z0))), 5'(4(z0)))
3'(0(4(3(5(4(3(0(1(z0))))))))) → c63(0'(3(0(3(4(3(2(4(5(1(z0)))))))))), 3'(0(3(4(3(2(4(5(1(z0))))))))), 0'(3(4(3(2(4(5(1(z0)))))))), 3'(4(3(2(4(5(1(z0))))))), 3'(2(4(5(1(z0))))), 5'(1(z0)))
3'(1(5(3(1(1(0(3(2(z0))))))))) → c64(5'(1(0(3(2(1(3(3(2(1(z0)))))))))), 0'(3(2(1(3(3(2(1(z0)))))))), 3'(2(1(3(3(2(1(z0))))))), 3'(3(2(1(z0)))), 3'(2(1(z0))))
3'(3(0(0(1(5(4(0(4(z0))))))))) → c65(0'(2(4(4(0(3(5(0(3(z0))))))))), 0'(3(5(0(3(z0))))), 3'(5(0(3(z0)))), 5'(0(3(z0))), 0'(3(z0)), 3'(z0))
3'(2(0(2(0(5(2(3(4(5(z0)))))))))) → c66(3'(5(4(4(2(0(3(2(5(2(0(z0))))))))))), 5'(4(4(2(0(3(2(5(2(0(z0)))))))))), 0'(3(2(5(2(0(z0)))))), 3'(2(5(2(0(z0))))), 5'(2(0(z0))), 0'(z0))
5'(0(4(z0))) → c67(0'(5(4(z0))), 5'(4(z0)))
5'(0(1(5(z0)))) → c68(0'(5(4(1(5(z0))))), 5'(4(1(5(z0)))), 5'(z0))
5'(2(3(1(z0)))) → c69(5'(2(1(3(z0)))), 3'(z0))
5'(2(3(5(z0)))) → c70(5'(3(5(z0))), 3'(5(z0)), 5'(z0))
5'(2(5(4(z0)))) → c71(5'(4(5(z0))), 5'(z0))
5'(2(3(1(4(z0))))) → c72(5'(2(1(2(1(3(4(z0))))))), 3'(4(z0)))
5'(3(0(0(4(z0))))) → c73(0'(0(3(5(4(4(z0)))))), 0'(3(5(4(4(z0))))), 3'(5(4(4(z0)))), 5'(4(4(z0))))
5'(0(1(2(3(1(z0)))))) → c74(0'(3(4(5(4(4(4(1(z0)))))))), 3'(4(5(4(4(4(1(z0))))))), 5'(4(4(4(1(z0))))))
5'(0(4(3(3(1(z0)))))) → c75(0'(3(5(1(5(4(4(3(z0)))))))), 3'(5(1(5(4(4(3(z0))))))), 5'(1(5(4(4(3(z0)))))), 5'(4(4(3(z0)))), 3'(z0))
5'(1(5(3(1(1(3(z0))))))) → c76(5'(1(5(1(3(3(z0)))))), 5'(1(3(3(z0)))), 3'(3(z0)), 3'(z0))
5'(2(0(0(1(0(3(z0))))))) → c77(0'(5(3(4(2(1(0(0(z0)))))))), 5'(3(4(2(1(0(0(z0))))))), 3'(4(2(1(0(0(z0)))))), 0'(0(z0)), 0'(z0))
5'(2(0(4(0(4(3(z0))))))) → c78(0'(5(1(0(4(4(3(z0))))))), 5'(1(0(4(4(3(z0)))))), 0'(4(4(3(z0)))), 3'(z0))
5'(2(3(0(0(4(3(z0))))))) → c79(0'(5(4(2(4(3(0(3(3(z0))))))))), 5'(4(2(4(3(0(3(3(z0)))))))), 3'(0(3(3(z0)))), 0'(3(3(z0))), 3'(3(z0)), 3'(z0))
5'(2(3(3(2(0(5(z0))))))) → c80(0'(3(3(5(2(4(5(z0))))))), 3'(3(5(2(4(5(z0)))))), 3'(5(2(4(5(z0))))), 5'(2(4(5(z0)))), 5'(z0))
5'(5(5(0(1(4(3(z0))))))) → c81(0'(5(4(4(3(4(5(5(1(z0))))))))), 5'(4(4(3(4(5(5(1(z0)))))))), 3'(4(5(5(1(z0))))), 5'(5(1(z0))), 5'(1(z0)))
5'(0(4(3(0(2(2(3(z0)))))))) → c82(0'(2(4(4(0(3(2(5(3(z0))))))))), 0'(3(2(5(3(z0))))), 3'(2(5(3(z0)))), 5'(3(z0)), 3'(z0))
5'(2(2(0(4(0(1(4(z0)))))))) → c83(0'(0(5(1(0(2(z0)))))), 0'(5(1(0(2(z0))))), 5'(1(0(2(z0)))), 0'(2(z0)))
5'(2(2(0(4(1(5(4(z0)))))))) → c84(5'(2(4(5(0(2(1(4(z0)))))))), 5'(0(2(1(4(z0))))), 0'(2(1(4(z0)))))
5'(3(2(2(1(1(0(5(z0)))))))) → c85(0'(3(2(5(2(1(5(1(2(z0))))))))), 3'(2(5(2(1(5(1(2(z0)))))))), 5'(2(1(5(1(2(z0)))))), 5'(1(2(z0))))
5'(2(0(3(1(2(5(0(4(z0))))))))) → c86(5'(1(0(3(5(2(4(2(4(0(z0)))))))))), 0'(3(5(2(4(2(4(0(z0)))))))), 3'(5(2(4(2(4(0(z0))))))), 5'(2(4(2(4(0(z0)))))), 0'(z0))
5'(2(0(3(2(0(4(4(1(z0))))))))) → c87(0'(5(3(0(5(2(2(4(2(4(1(z0))))))))))), 5'(3(0(5(2(2(4(2(4(1(z0)))))))))), 3'(0(5(2(2(4(2(4(1(z0))))))))), 0'(5(2(2(4(2(4(1(z0)))))))), 5'(2(2(4(2(4(1(z0))))))))
5'(5(0(1(1(3(2(5(2(z0))))))))) → c88(3'(5(1(2(2(0(5(1(5(4(z0)))))))))), 5'(1(2(2(0(5(1(5(4(z0))))))))), 0'(5(1(5(4(z0))))), 5'(1(5(4(z0)))), 5'(4(z0)))
5'(5(3(2(1(0(1(0(4(z0))))))))) → c89(0'(2(1(3(5(0(5(4(2(4(1(z0))))))))))), 3'(5(0(5(4(2(4(1(z0)))))))), 5'(0(5(4(2(4(1(z0))))))), 0'(5(4(2(4(1(z0)))))), 5'(4(2(4(1(z0))))))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(0(1(z0))) → 0(0(2(1(z0))))
0(1(3(z0))) → 0(3(4(1(z0))))
0(0(0(1(z0)))) → 0(0(0(2(1(z0)))))
0(0(1(5(z0)))) → 0(0(5(1(2(4(z0))))))
0(0(5(3(z0)))) → 0(0(5(4(3(z0)))))
0(4(1(1(z0)))) → 0(5(4(1(2(1(z0))))))
0(4(3(1(z0)))) → 0(3(5(4(1(z0)))))
0(4(3(4(z0)))) → 0(3(2(4(4(z0)))))
0(1(2(2(1(z0))))) → 2(4(0(1(2(1(z0))))))
0(1(5(0(4(z0))))) → 0(2(1(5(4(0(z0))))))
0(1(5(5(3(z0))))) → 0(5(4(5(1(3(z0))))))
0(2(2(1(5(z0))))) → 0(2(1(5(4(2(4(4(2(z0)))))))))
0(2(2(3(4(z0))))) → 0(3(4(4(2(4(4(2(z0))))))))
0(2(5(1(1(z0))))) → 5(0(1(2(4(1(z0))))))
0(3(3(2(3(z0))))) → 0(3(3(2(4(3(z0))))))
0(4(4(3(4(z0))))) → 4(4(4(4(0(3(z0))))))
0(1(3(4(3(4(z0)))))) → 0(3(4(3(4(1(2(z0)))))))
0(1(5(0(4(2(z0)))))) → 0(5(2(4(1(0(2(z0)))))))
0(2(2(2(3(1(z0)))))) → 0(2(2(4(2(3(1(z0)))))))
0(4(1(1(0(4(z0)))))) → 0(4(4(1(4(1(0(z0)))))))
0(4(3(2(2(3(z0)))))) → 0(2(3(2(4(2(3(z0)))))))
0(0(1(1(3(3(3(z0))))))) → 0(3(0(1(3(3(4(1(z0))))))))
0(0(2(5(1(4(2(z0))))))) → 0(2(1(0(5(4(2(2(z0))))))))
0(2(5(4(4(1(5(z0))))))) → 1(2(4(5(0(5(4(4(z0))))))))
0(4(2(3(4(5(4(z0))))))) → 3(0(5(4(4(2(4(0(z0))))))))
0(5(2(1(2(1(4(z0))))))) → 2(1(2(1(0(5(2(4(z0))))))))
0(2(0(5(5(2(2(3(z0)))))))) → 5(2(2(4(5(3(2(0(0(z0)))))))))
0(2(5(2(4(0(1(4(z0)))))))) → 0(3(0(5(2(1(2(2(4(4(z0))))))))))
0(4(1(5(3(2(3(3(z0)))))))) → 0(5(4(1(2(3(3(4(3(z0)))))))))
0(4(5(0(1(5(2(3(z0)))))))) → 2(1(2(4(2(5(3(0(5(0(z0))))))))))
0(5(5(1(4(2(0(3(z0)))))))) → 0(3(5(1(2(0(5(1(2(4(z0))))))))))
0(0(4(4(5(3(1(1(5(z0))))))))) → 2(1(5(4(4(4(1(0(0(3(5(z0)))))))))))
0(1(2(5(1(4(0(3(4(z0))))))))) → 0(2(4(0(3(1(2(1(2(4(5(z0)))))))))))
0(1(3(1(2(0(1(1(5(z0))))))))) → 0(5(1(0(1(4(1(1(2(3(z0))))))))))
0(2(0(4(1(5(3(0(4(z0))))))))) → 4(1(0(3(5(0(0(2(2(4(z0))))))))))
0(4(3(3(4(2(5(0(5(z0))))))))) → 0(5(0(4(3(2(4(5(3(2(z0))))))))))
0(1(3(1(4(2(0(4(5(2(z0)))))))))) → 4(0(1(2(4(0(2(1(5(1(3(z0)))))))))))
0(4(3(1(3(5(2(5(4(4(z0)))))))))) → 0(5(5(2(4(4(1(5(4(3(3(z0)))))))))))
3(1(1(z0))) → 3(1(4(1(z0))))
3(1(1(z0))) → 3(4(1(4(4(1(z0))))))
3(1(1(z0))) → 3(4(4(1(2(4(1(z0)))))))
3(3(1(z0))) → 3(2(1(3(z0))))
3(0(1(1(z0)))) → 0(2(1(3(1(z0)))))
3(1(1(5(z0)))) → 3(1(2(1(5(z0)))))
3(0(1(4(3(z0))))) → 3(2(0(3(4(1(z0))))))
3(0(4(5(1(z0))))) → 3(5(4(4(1(0(z0))))))
3(1(1(1(2(z0))))) → 3(2(1(4(1(2(1(2(z0))))))))
3(0(4(1(2(2(z0)))))) → 3(2(1(0(4(4(2(z0)))))))
3(1(0(3(5(4(z0)))))) → 3(0(3(2(1(5(4(z0)))))))
3(2(2(1(1(3(z0)))))) → 1(2(1(3(2(4(3(z0)))))))
3(3(3(1(3(5(z0)))))) → 3(2(1(3(3(3(5(z0)))))))
3(4(3(0(4(5(z0)))))) → 3(5(0(3(4(4(4(z0)))))))
3(4(3(1(4(2(z0)))))) → 3(4(2(1(3(2(2(4(2(4(z0))))))))))
3(5(0(2(1(4(z0)))))) → 3(2(4(0(5(1(2(z0)))))))
3(5(5(2(3(1(z0)))))) → 5(5(4(3(3(2(1(z0)))))))
3(2(5(0(4(0(1(z0))))))) → 0(0(5(4(2(2(4(4(1(3(z0))))))))))
3(4(3(4(0(1(4(z0))))))) → 3(4(2(4(4(4(0(5(1(2(3(z0)))))))))))
3(5(2(1(0(2(2(z0))))))) → 2(1(3(0(5(2(2(4(z0))))))))
3(5(2(2(0(1(1(z0))))))) → 3(2(4(5(0(2(1(2(1(z0)))))))))
3(5(3(4(0(1(4(z0))))))) → 2(1(5(4(3(4(0(3(z0))))))))
3(0(1(3(2(0(4(2(z0)))))))) → 0(4(2(2(2(4(1(0(3(3(4(z0)))))))))))
3(3(1(1(2(5(5(2(z0)))))))) → 3(2(1(5(1(2(5(3(1(z0)))))))))
3(5(4(2(5(1(0(4(z0)))))))) → 4(2(4(2(1(3(5(0(5(4(z0))))))))))
3(0(4(3(5(4(3(0(1(z0))))))))) → 0(3(0(3(4(3(2(4(5(1(z0))))))))))
3(1(5(3(1(1(0(3(2(z0))))))))) → 5(1(0(3(2(1(3(3(2(1(z0))))))))))
3(3(0(0(1(5(4(0(4(z0))))))))) → 1(0(2(4(4(0(3(5(0(3(z0))))))))))
3(2(0(2(0(5(2(3(4(5(z0)))))))))) → 3(5(4(4(2(0(3(2(5(2(0(z0)))))))))))
5(0(4(z0))) → 4(0(5(4(z0))))
5(0(1(5(z0)))) → 0(5(4(1(5(z0)))))
5(2(3(1(z0)))) → 4(5(2(1(3(z0)))))
5(2(3(5(z0)))) → 2(4(5(3(5(z0)))))
5(2(5(4(z0)))) → 2(4(5(4(5(z0)))))
5(2(3(1(4(z0))))) → 5(2(1(2(1(3(4(z0)))))))
5(3(0(0(4(z0))))) → 0(0(3(5(4(4(z0))))))
5(0(1(2(3(1(z0)))))) → 2(1(0(3(4(5(4(4(4(1(z0))))))))))
5(0(4(3(3(1(z0)))))) → 0(3(5(1(5(4(4(3(z0))))))))
5(1(5(3(1(1(3(z0))))))) → 2(1(5(1(5(1(3(3(z0))))))))
5(2(0(0(1(0(3(z0))))))) → 0(5(3(4(2(1(0(0(z0))))))))
5(2(0(4(0(4(3(z0))))))) → 2(0(5(1(0(4(4(3(z0))))))))
5(2(3(0(0(4(3(z0))))))) → 0(5(4(2(4(3(0(3(3(z0)))))))))
5(2(3(3(2(0(5(z0))))))) → 2(0(3(3(5(2(4(5(z0))))))))
5(5(5(0(1(4(3(z0))))))) → 0(5(4(4(3(4(5(5(1(z0)))))))))
5(0(4(3(0(2(2(3(z0)))))))) → 0(2(4(4(0(3(2(5(3(z0)))))))))
5(2(2(0(4(0(1(4(z0)))))))) → 4(2(4(0(0(5(1(0(2(z0)))))))))
5(2(2(0(4(1(5(4(z0)))))))) → 2(5(2(4(5(0(2(1(4(z0)))))))))
5(3(2(2(1(1(0(5(z0)))))))) → 0(3(2(5(2(1(5(1(2(z0)))))))))
5(2(0(3(1(2(5(0(4(z0))))))))) → 5(1(0(3(5(2(4(2(4(0(z0))))))))))
5(2(0(3(2(0(4(4(1(z0))))))))) → 0(5(3(0(5(2(2(4(2(4(1(z0)))))))))))
5(5(0(1(1(3(2(5(2(z0))))))))) → 3(5(1(2(2(0(5(1(5(4(z0))))))))))
5(5(3(2(1(0(1(0(4(z0))))))))) → 0(2(1(3(5(0(5(4(2(4(1(z0)))))))))))
Tuples:
0'(4(1(1(z0)))) → c5(0'(5(4(1(2(1(z0)))))), 5'(4(1(2(1(z0))))))
0'(1(2(2(1(z0))))) → c8(0'(1(2(1(z0)))))
3'(1(1(z0))) → c38(3'(1(4(1(z0)))))
3'(1(1(z0))) → c39(3'(4(1(4(4(1(z0)))))))
3'(1(1(z0))) → c40(3'(4(4(1(2(4(1(z0))))))))
3'(1(1(1(2(z0))))) → c46(3'(2(1(4(1(2(1(2(z0)))))))))
S tuples:
0'(4(1(1(z0)))) → c5(0'(5(4(1(2(1(z0)))))), 5'(4(1(2(1(z0))))))
0'(1(2(2(1(z0))))) → c8(0'(1(2(1(z0)))))
3'(1(1(z0))) → c38(3'(1(4(1(z0)))))
3'(1(1(z0))) → c39(3'(4(1(4(4(1(z0)))))))
3'(1(1(z0))) → c40(3'(4(4(1(2(4(1(z0))))))))
3'(1(1(1(2(z0))))) → c46(3'(2(1(4(1(2(1(2(z0)))))))))
K tuples:none
Defined Rule Symbols:
0, 3, 5
Defined Pair Symbols:
0', 3'
Compound Symbols:
c5, c8, c38, c39, c40, c46
(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 6 of 6 dangling nodes:
3'(1(1(z0))) → c38(3'(1(4(1(z0)))))
0'(4(1(1(z0)))) → c5(0'(5(4(1(2(1(z0)))))), 5'(4(1(2(1(z0))))))
0'(1(2(2(1(z0))))) → c8(0'(1(2(1(z0)))))
3'(1(1(z0))) → c39(3'(4(1(4(4(1(z0)))))))
3'(1(1(z0))) → c40(3'(4(4(1(2(4(1(z0))))))))
3'(1(1(1(2(z0))))) → c46(3'(2(1(4(1(2(1(2(z0)))))))))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(0(1(z0))) → 0(0(2(1(z0))))
0(1(3(z0))) → 0(3(4(1(z0))))
0(0(0(1(z0)))) → 0(0(0(2(1(z0)))))
0(0(1(5(z0)))) → 0(0(5(1(2(4(z0))))))
0(0(5(3(z0)))) → 0(0(5(4(3(z0)))))
0(4(1(1(z0)))) → 0(5(4(1(2(1(z0))))))
0(4(3(1(z0)))) → 0(3(5(4(1(z0)))))
0(4(3(4(z0)))) → 0(3(2(4(4(z0)))))
0(1(2(2(1(z0))))) → 2(4(0(1(2(1(z0))))))
0(1(5(0(4(z0))))) → 0(2(1(5(4(0(z0))))))
0(1(5(5(3(z0))))) → 0(5(4(5(1(3(z0))))))
0(2(2(1(5(z0))))) → 0(2(1(5(4(2(4(4(2(z0)))))))))
0(2(2(3(4(z0))))) → 0(3(4(4(2(4(4(2(z0))))))))
0(2(5(1(1(z0))))) → 5(0(1(2(4(1(z0))))))
0(3(3(2(3(z0))))) → 0(3(3(2(4(3(z0))))))
0(4(4(3(4(z0))))) → 4(4(4(4(0(3(z0))))))
0(1(3(4(3(4(z0)))))) → 0(3(4(3(4(1(2(z0)))))))
0(1(5(0(4(2(z0)))))) → 0(5(2(4(1(0(2(z0)))))))
0(2(2(2(3(1(z0)))))) → 0(2(2(4(2(3(1(z0)))))))
0(4(1(1(0(4(z0)))))) → 0(4(4(1(4(1(0(z0)))))))
0(4(3(2(2(3(z0)))))) → 0(2(3(2(4(2(3(z0)))))))
0(0(1(1(3(3(3(z0))))))) → 0(3(0(1(3(3(4(1(z0))))))))
0(0(2(5(1(4(2(z0))))))) → 0(2(1(0(5(4(2(2(z0))))))))
0(2(5(4(4(1(5(z0))))))) → 1(2(4(5(0(5(4(4(z0))))))))
0(4(2(3(4(5(4(z0))))))) → 3(0(5(4(4(2(4(0(z0))))))))
0(5(2(1(2(1(4(z0))))))) → 2(1(2(1(0(5(2(4(z0))))))))
0(2(0(5(5(2(2(3(z0)))))))) → 5(2(2(4(5(3(2(0(0(z0)))))))))
0(2(5(2(4(0(1(4(z0)))))))) → 0(3(0(5(2(1(2(2(4(4(z0))))))))))
0(4(1(5(3(2(3(3(z0)))))))) → 0(5(4(1(2(3(3(4(3(z0)))))))))
0(4(5(0(1(5(2(3(z0)))))))) → 2(1(2(4(2(5(3(0(5(0(z0))))))))))
0(5(5(1(4(2(0(3(z0)))))))) → 0(3(5(1(2(0(5(1(2(4(z0))))))))))
0(0(4(4(5(3(1(1(5(z0))))))))) → 2(1(5(4(4(4(1(0(0(3(5(z0)))))))))))
0(1(2(5(1(4(0(3(4(z0))))))))) → 0(2(4(0(3(1(2(1(2(4(5(z0)))))))))))
0(1(3(1(2(0(1(1(5(z0))))))))) → 0(5(1(0(1(4(1(1(2(3(z0))))))))))
0(2(0(4(1(5(3(0(4(z0))))))))) → 4(1(0(3(5(0(0(2(2(4(z0))))))))))
0(4(3(3(4(2(5(0(5(z0))))))))) → 0(5(0(4(3(2(4(5(3(2(z0))))))))))
0(1(3(1(4(2(0(4(5(2(z0)))))))))) → 4(0(1(2(4(0(2(1(5(1(3(z0)))))))))))
0(4(3(1(3(5(2(5(4(4(z0)))))))))) → 0(5(5(2(4(4(1(5(4(3(3(z0)))))))))))
3(1(1(z0))) → 3(1(4(1(z0))))
3(1(1(z0))) → 3(4(1(4(4(1(z0))))))
3(1(1(z0))) → 3(4(4(1(2(4(1(z0)))))))
3(3(1(z0))) → 3(2(1(3(z0))))
3(0(1(1(z0)))) → 0(2(1(3(1(z0)))))
3(1(1(5(z0)))) → 3(1(2(1(5(z0)))))
3(0(1(4(3(z0))))) → 3(2(0(3(4(1(z0))))))
3(0(4(5(1(z0))))) → 3(5(4(4(1(0(z0))))))
3(1(1(1(2(z0))))) → 3(2(1(4(1(2(1(2(z0))))))))
3(0(4(1(2(2(z0)))))) → 3(2(1(0(4(4(2(z0)))))))
3(1(0(3(5(4(z0)))))) → 3(0(3(2(1(5(4(z0)))))))
3(2(2(1(1(3(z0)))))) → 1(2(1(3(2(4(3(z0)))))))
3(3(3(1(3(5(z0)))))) → 3(2(1(3(3(3(5(z0)))))))
3(4(3(0(4(5(z0)))))) → 3(5(0(3(4(4(4(z0)))))))
3(4(3(1(4(2(z0)))))) → 3(4(2(1(3(2(2(4(2(4(z0))))))))))
3(5(0(2(1(4(z0)))))) → 3(2(4(0(5(1(2(z0)))))))
3(5(5(2(3(1(z0)))))) → 5(5(4(3(3(2(1(z0)))))))
3(2(5(0(4(0(1(z0))))))) → 0(0(5(4(2(2(4(4(1(3(z0))))))))))
3(4(3(4(0(1(4(z0))))))) → 3(4(2(4(4(4(0(5(1(2(3(z0)))))))))))
3(5(2(1(0(2(2(z0))))))) → 2(1(3(0(5(2(2(4(z0))))))))
3(5(2(2(0(1(1(z0))))))) → 3(2(4(5(0(2(1(2(1(z0)))))))))
3(5(3(4(0(1(4(z0))))))) → 2(1(5(4(3(4(0(3(z0))))))))
3(0(1(3(2(0(4(2(z0)))))))) → 0(4(2(2(2(4(1(0(3(3(4(z0)))))))))))
3(3(1(1(2(5(5(2(z0)))))))) → 3(2(1(5(1(2(5(3(1(z0)))))))))
3(5(4(2(5(1(0(4(z0)))))))) → 4(2(4(2(1(3(5(0(5(4(z0))))))))))
3(0(4(3(5(4(3(0(1(z0))))))))) → 0(3(0(3(4(3(2(4(5(1(z0))))))))))
3(1(5(3(1(1(0(3(2(z0))))))))) → 5(1(0(3(2(1(3(3(2(1(z0))))))))))
3(3(0(0(1(5(4(0(4(z0))))))))) → 1(0(2(4(4(0(3(5(0(3(z0))))))))))
3(2(0(2(0(5(2(3(4(5(z0)))))))))) → 3(5(4(4(2(0(3(2(5(2(0(z0)))))))))))
5(0(4(z0))) → 4(0(5(4(z0))))
5(0(1(5(z0)))) → 0(5(4(1(5(z0)))))
5(2(3(1(z0)))) → 4(5(2(1(3(z0)))))
5(2(3(5(z0)))) → 2(4(5(3(5(z0)))))
5(2(5(4(z0)))) → 2(4(5(4(5(z0)))))
5(2(3(1(4(z0))))) → 5(2(1(2(1(3(4(z0)))))))
5(3(0(0(4(z0))))) → 0(0(3(5(4(4(z0))))))
5(0(1(2(3(1(z0)))))) → 2(1(0(3(4(5(4(4(4(1(z0))))))))))
5(0(4(3(3(1(z0)))))) → 0(3(5(1(5(4(4(3(z0))))))))
5(1(5(3(1(1(3(z0))))))) → 2(1(5(1(5(1(3(3(z0))))))))
5(2(0(0(1(0(3(z0))))))) → 0(5(3(4(2(1(0(0(z0))))))))
5(2(0(4(0(4(3(z0))))))) → 2(0(5(1(0(4(4(3(z0))))))))
5(2(3(0(0(4(3(z0))))))) → 0(5(4(2(4(3(0(3(3(z0)))))))))
5(2(3(3(2(0(5(z0))))))) → 2(0(3(3(5(2(4(5(z0))))))))
5(5(5(0(1(4(3(z0))))))) → 0(5(4(4(3(4(5(5(1(z0)))))))))
5(0(4(3(0(2(2(3(z0)))))))) → 0(2(4(4(0(3(2(5(3(z0)))))))))
5(2(2(0(4(0(1(4(z0)))))))) → 4(2(4(0(0(5(1(0(2(z0)))))))))
5(2(2(0(4(1(5(4(z0)))))))) → 2(5(2(4(5(0(2(1(4(z0)))))))))
5(3(2(2(1(1(0(5(z0)))))))) → 0(3(2(5(2(1(5(1(2(z0)))))))))
5(2(0(3(1(2(5(0(4(z0))))))))) → 5(1(0(3(5(2(4(2(4(0(z0))))))))))
5(2(0(3(2(0(4(4(1(z0))))))))) → 0(5(3(0(5(2(2(4(2(4(1(z0)))))))))))
5(5(0(1(1(3(2(5(2(z0))))))))) → 3(5(1(2(2(0(5(1(5(4(z0))))))))))
5(5(3(2(1(0(1(0(4(z0))))))))) → 0(2(1(3(5(0(5(4(2(4(1(z0)))))))))))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
0, 3, 5
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))